This PR contains a way to treat the unspecified bits that result from e.g. out-directed parameters and gets rid of ARB everywhere in HOL4P4. Each unspecified bit is modeled here as an indexed call to an oracle function for random bits, e.g. an uninitialised bitvector of length four would be represented as [oracle 1; oracle 2; oracle 3; oracle 4], where oracle is the random oracle function. The top-level static environment now contains the random oracle function, as well as a getter and setter for the oracle index. The static environment of the expression-level semantics does not contain the getter and setter, but only the oracle index. Additionally, the expression-level semantics may now return an updated oracle index in addition to the new function frame.

Having a separate static environment on the expression-level is also desirable since this allows to eliminate some unused components (parser state map, table map), but this is for a later PR.

Organizationally, this PR also puts the metatheory in a separate subdirectory and adds the compilation of this subdirectory to the CI. This allows for quicker iterations when making changes to the base hol directory, e.g. to the architectural models.